T:Type, eq:EqDecider(T), L:(T List).
no_repeats(T;L)  Inj({x:T| (x  L)} ;{0..||L||};x.index(L;x)) 

latex

Definitions	t  T, P  Q, x:A. B(x), index(L;x), ||as||, #$n, {i..j}, s = t, , (x  l), {x:A| B(x)} , , A  B, a < b, x:A  B(x), P & Q, i  j < k, True, T, x:AB(x), Inj(A;B;f), Type, EqDecider(T), type List, no_repeats(T;l), A, , s ~ t, {T}, False, SQType(T), A c B, x:A. B(x), Void, l[i], P  Q, P  Q
Lemmas	select wf, squash wf, no repeats l index, select member, le wf, no repeats wf, deq wf, l member wf, int seg wf, length wf1, l index wf